$\forall$$A$:Type, $X$:MaInterface($A$), ${\it es}$:ES.
\\[0ex]ma{-}interface{-}consistent(${\it es}$;$X$)
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. ($\uparrow$($e$ $\in_{b}$ [[$X$]])) $\Rightarrow$ (loc($e$) $\in$ ma{-}interface{-}locs($X$)))